(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
turing(I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog) → turing[Ite](!EQ(x, i1), I(IfGoto(i1, i2), r), revltape, Cons(x, xs), prog)
turing(I(Goto(int), r), revltape, rtape, prog) → turing(lookup(int, prog), revltape, rtape, prog)
turing(I(Right, r), revltape, Cons(x, xs), prog) → turing(r, Cons(x, revltape), xs, prog)
turing(I(Right, r), revltape, Nil, prog) → turing(r, Cons(0, revltape), Nil, prog)
turing(I(Left, r), Cons(x, xs), rtape, prog) → turing(r, xs, Cons(x, rtape), prog)
turing(I(Left, r), Nil, rtape, prog) → turing(r, Nil, Cons(0, rtape), prog)
turing(I(Write(int), r), revltape, Cons(x, xs), prog) → turing(r, revltape, Cons(int, xs), prog)
turing(I(Halt, r), revltape, rtape, prog) → rtape
turing(Empty, revltape, rtape, prog) → rtape
lookup(S(x), I(l, r)) → lookup(x, r)
instrsConstrCheck(I(l1, r1), I(x, y)) → True
instrsConstrCheck(I(l1, r1), Empty) → False
instrsConstrCheck(Empty, I(x, y)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True
instrConstrCheck(Goto(gtNat), Right) → False
instrConstrCheck(Goto(gtNat), Left) → False
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False
instrConstrCheck(Goto(gtNat), Halt) → False
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Right, Goto(gtNat2)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(wNat2)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Left, Goto(gtNat2)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(wNat2)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False
instrConstrCheck(Write(wNat), Right) → False
instrConstrCheck(Write(wNat), Left) → False
instrConstrCheck(Write(wNat), Write(wNat2)) → True
instrConstrCheck(Write(wNat), Halt) → False
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False
instrConstrCheck(Halt, Goto(gtNat2)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(wNat2)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lookup(0, instrs) → instrs
instrsSecond(I(l, r)) → r
instrsFirst(I(l, r)) → l
getWrite(Write(int)) → int
getGotoSecond(IfGoto(i1, i2)) → i2
getGotoFirst(IfGoto(i1, i2)) → i1
getGoto(Goto(int)) → int
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)
The (relative) TRS S consists of the following rules:
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
turing[Ite](True, I(IfGoto(i1, i2), r), revltape, rtape, prog) → turing(lookup(i2, prog), revltape, rtape, prog)
turing[Ite](False, I(l, r), revltape, rtape, prog) → turing(r, revltape, rtape, prog)
Rewrite Strategy: INNERMOST
(1) InfiniteLowerBoundProof (EQUIVALENT transformation)
The loop following loop proves infinite runtime complexity:
The rewrite sequence
turing(I(Goto(0), r), revltape, rtape, I(Goto(0), r25489_3)) →+ turing(I(Goto(0), r25489_3), revltape, rtape, I(Goto(0), r25489_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [ ].
The result substitution is [r / r25489_3].
(2) BOUNDS(INF, INF)